module MeteoCal

//SIGNATURES

sig User{
		username: one User,
		calendar: one Calendar,
		invitates: set User
}

sig Calendar{
		importer: one User,
		exporter: one User,
		event: set Event
}

sig Event{
		id: one Event,
		starttime: one Time,
		endtime: one Time,
		participant: set User,
		creator: one User,
		deleter: one User,
		updater: one User,
		weather: one WeatherInformation
}

sig Time{
		value: Int
}{
	value >0
}

sig WeatherNotification{
		event: set OutdoorEvent,
		receiver: set User
}{
		#event >0
}

sig IndoorEvent extends Event{}

sig OutdoorEvent extends Event{}

sig Invitation{
		event: one Event,
		sender: one User,
		receiver: set User
 }{
		#receiver >0
}

sig WeatherInformation{
		notification: set WeatherNotification
}

//FACTS

fact UserProperties{
		//Users cannot have the same Username
		no disj u1, u2: User | u1.username = u2.username
		//User cannot be invited by himself
		no u: User | u in u.invitates
		/*If A is the creator (and so updater and deleter too) of E, then B
 cannot be the creator(and so updater and deleter too) of E*/
		no disj u1, u2: User | one e: Event |
				u1 = e.creator && u1 = e.updater && u1 = e.deleter implies 
				u2 = e.creator && u2 = e.updater && u2 = e.deleter
		//User cannot receive more than one invitation for the same event.
		no disj i1, i2: Invitation | one u: User |
				u = i1.receiver && u = i2.receiver && i1.event = i2.event
		//User can export just his calendar
		no disj c1, c2: Calendar | one u: User |
				c1.exporter = u && c2.exporter = u && u.calendar = c1 && u.calendar = c2
		//User can import just his calendar
		no disj c1, c2: Calendar | one u: User |
				c1.importer = u && c2.importer = u && u.calendar = c1 && u.calendar = c2
}



fact OutdoorEventProperties{
		//If there exists an outdoor event, it exists a weather notification too
		all o: OutdoorEvent | all wn: WeatherNotification | all u: User |
			o.creator = u implies wn.event = o
}

fact EventProperties{
		//Events cannot have the same id
		no disj e1, e2: Event | e1.id = e2.id
		//If an event A is outdoor it is not indoor
		no e: Event | one i: IndoorEvent | one o: OutdoorEvent |
				e = i && e = o
		//Each event has one related invitation
		no disj i1, i2: Invitation | one e: Event |
				i1.event = e && i2.event = e
		//Each user cannot participate to overlapped events
		all u: User | no disj e1, e2: Event | e1.participant = u && e2.participant = u &&
 e1.endtime.value > e2.starttime.value || e2.endtime.value > e1.starttime.value
}

fact InvitationProperties{
		//One invitation has just one sender
		no disj u1, u2: User | one i: Invitation |
				i.sender = u1 && i.sender = u2
}

fact CalendarProperties{
		//User can have just one calendar
		no disj c1, c2: Calendar | one u: User |
				u.calendar = c1 && u.calendar = c2
}



//ASSERTIONS


assert NoInvitedbyHimself{
		no u: User | u in u.invitates
}

check NoInvitedbyHimself  

assert NoMoreInvitation{
		no disj i1, i2: Invitation | one u: User |
				u = i1.receiver && u = i2.receiver && i1.event = i2.event
}

check NoMoreInvitation  

assert NoMoreCalendarExported{
		no disj c1, c2: Calendar | one u: User |
				c1.exporter = u && c2.exporter = u && u.calendar = c1 && u.calendar = c2
}

check NoMoreCalendarExported  

assert OutDoorEvent{
		all o: OutdoorEvent | all wn: WeatherNotification | all u: User |
			o.creator = u implies wn.event = o
}

check OutDoorEvent  

//PREDICATE

pred showEvent(){
		#Event > #OutdoorEvent
}

run showEvent for 2 but exactly 2 Event, 1 OutdoorEvent  

pred showUser(){}

run showUser for 4

pred show() {}

run show for 2

pred showCalendar(){}

run showCalendar for 2
